#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)

/* Toutes les obligations de preuve sont validées */



/*@ predicate isMin (int *a, integer n,integer x) = 
  @   \forall integer k;(0<=k<n) ==> (a[k] >= a[x]);
  @*/

/*@ predicate oneValue(int *a, integer n) =
  @   \forall integer k; (0<=k<n) ==> (a[k] == a[0]);
  @*/

/*@ predicate is2ndMin (int *a, integer n, integer x) =
  @   \forall integer l; (0<=l<n && a[l]<a[x]) ==> isMin(a, n, l);
  @*/

/*@
  @ requires n >= 2;
  @ requires \valid_range(a,0,n-1);
  @ ensures -1<=\result<n;
  @ ensures (\result == -1) ==> oneValue(a,n);
  @ ensures (0<=\result<n && !isMin(a,n,\result) && is2ndMin(a, n, \result)) ==> !oneValue(a,n); 
  @*/
int arraymin2(int * a, int n) {
  int i, imin1, imin2;
 
  imin1 = 0; imin2 = -1;

  /*@ 
    @ loop invariant 1<=i<=n;
    @ loop invariant 0<=imin1<i;
    @ loop invariant -1<=imin2<i;
    @ loop invariant imin2 != imin1;
    @ loop invariant isMin(a,i,imin1);
    @ loop invariant (imin2 == -1) ==> oneValue(a,i);
    @ loop invariant (imin2 != -1) ==> !isMin(a,i,imin2);
    @ loop invariant (imin2 != -1) ==> is2ndMin(a,i,imin2);
    @ loop variant n-i;
    @*/
  for(i = 1; i < n; ++i){
    // If current element is smaller than current minimal, update both
    if (a[i] < a[imin1]) {
      imin2 = imin1;
      imin1 = i;
    }
    // If it is between minimal and 2nd minimal, update the latter
    else if ((a[imin1] < a[i]) && ((imin2 == -1) || (a[i] < a[imin2])))
      imin2 = i;
  }

  return imin2;
}
